In mathematics, S2S is the monadic second order theory with two successors. It is one of the most expressive natural decidable theories known, with many decidable theories interpretable in S2S. Its decidability was proved by

Rabin Rabin is a List of Jewish surnames, Hebrew surname. It originates from the Hebrew word ''rav'' meaning Rabbi, or from the name of the specific Rabbi Abin I, Abin. The most well known bearer of the name was Yitzhak Rabin, prime minister of Israel ...

in 1969.

Basic properties

The first order objects of S2S are finite binary strings. The second order objects are arbitrary sets (or unary predicates) of finite binary strings. S2S has functions ''s''→''s''0 and ''s''→''s''1 on strings, and predicate ''s''∈''S'' (equivalently, ''S''(''s'')) meaning string ''s'' belongs to set ''S''. Some properties and conventions: * By default, lowercase letters refer to first order objects, and uppercase to second order objects. * The inclusion of sets makes S2S second order, with "monadic" indicating absence of ''k''-ary predicate variables for ''k''>1. * Concatenation of strings ''s'' and ''t'' is denoted by ''st'', and is ''not'' generally available in S2S, not even ''s''→0''s''. The

prefix relation In computer science, in the area of formal language theory, frequent use is made of a variety of string functions; however, the notation used is different from that used for computer programming, and some commonly used functions in the theoretical r ...

between strings is definable. * Equality is primitive, or it can be defined as ''s'' = ''t'' ⇔ ∀''S'' (''S''(''s'') ⇔ ''S''(''t'')) and ''S'' = ''T'' ⇔ ∀''s'' (''S''(''s'') ⇔ ''T''(''s'')). * In place of strings, one can use (for example) natural numbers with ''n''→2''n''+1 and ''n''→2''n''+2 but no other operations. * The set of all binary strings is denoted by ^*, using

Kleene star In mathematical logic and computer science, the Kleene star (or Kleene operator or Kleene closure) is a unary operation, either on sets of strings or on sets of symbols or characters. In mathematics, it is more commonly known as the free monoid c ...

. * Arbitrary subsets of ^* are sometimes identified with trees, specifically as a -labeled tree ^*; ^* forms a complete infinite binary tree. * For formula complexity, the prefix relation on strings is typically treated as first order. Without it, not all formulas would be equivalent to Δ¹₂ formulas. * For properties expressible in S2S (viewing the set of all binary strings as a tree), for each node, only ''O''(1) bits can be communicated between the left subtree and the right subtree and the rest (see

communication complexity In theoretical computer science, communication complexity studies the amount of communication required to solve a problem when the input to the problem is distributed among two or more parties. The study of communication complexity was first intro ...

). * For a fixed ''k'', a function from strings to ''k'' (i.e. natural numbers below ''k'') can be encoded by a single set. Moreover, ''s'',''t'' ⇒ ''s''01''t'' where ''t'' doubles every character of ''t'' is injective, and ''s'' ⇒ is S2S definable. By contrast, by a communication complexity argument, in S1S (below) a pair of sets is not encodable by a single set. ''Weakenings of S2S:'' Weak S2S (WS2S) requires all sets to be finite (note that finiteness is expressible in S2S using

Kőnig's lemma Kőnig's lemma or Kőnig's infinity lemma is a theorem in graph theory due to the Hungarian mathematician Dénes Kőnig who published it in 1927. It gives a sufficient condition for an infinite graph to have an infinitely long path. The computab ...

). S1S can be obtained by requiring that '1' does not appear in strings, and WS1S also requires finiteness. Even WS1S can interpret

Presburger arithmetic Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitti ...

with a predicate for powers of 2, as sets can be used to represent unbounded binary numbers with definable addition. Decision complexity S2S is decidable, and each of S2S, S1S, WS2S, WS1S has a nonelementary decision complexity corresponding to a linearly growing stack of exponentials. For the lower bound, it suffices to consider Σ¹₁ WS1S sentences. A single second order quantifier can be used to propose an arithmetic (or other) computation, which can be verified using first order quantifiers if we can test which numbers are equal. For this, if we appropriately encode numbers 1..''m'', we can encode a number with binary representation ''i''₁''i''₂...''i''_''m'' as ''i''₁ 1 ''i''₂ 2 ... ''i''_''m'' ''m'', preceded by a guard. By merging testing of guards and reusing variable names, the number of bits is linear in the number of exponentials. For the upper bound, using the decision procedure (below), sentences with ''k''-fold quantifier alternation can decided in time corresponding to ''k''+''O''(1)-fold exponentiation of the sentence length (with uniform constants). Axiomatization WS2S can be axiomatized through certain basic properties plus induction schema. S2S can be partially axiomatized by:
(1) ∃!''s'' ∀''t'' ( ''t''0≠''s'' ∧ ''t''1≠''s'') (empty string, denoted by ε; ∃!''s'' means "there is unique ''s''")
(2) ∀''s'',''t'' ∀''i''∈ ∀''j''∈ (''si''=''tj'' ⇒ ''s''=''t'' ∧ ''i''=''j'') (the use of ''i'' and ''j'' is an abbreviation; for ''i''=''j'', 0 does not equal 1)
(3) ∀''S'' (''S''(ε) ∧ ∀''s'' (''S''(''s'') ⇒ ''S''(''s''0) ∧ ''S''(''s''1))⇒ ∀''s'' ''S''(s)) (

induction Induction, Inducible or Inductive may refer to: Biology and medicine * Labor induction (birth/pregnancy) * Induction chemotherapy, in medicine * Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...

)
(4) ∃''S'' ∀''s'' (''S''(''s'') ⇔ φ(''s'')) (''S'' not free in φ) (4) is the comprehension schema over formulas φ, which always holds for second order logic. As usual, if φ has free variables not shown, we take the universal closure of the axiom. If equality is primitive for predicates, one also adds

extensionality In logic, extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties. It stands in contrast to the concept of intensionality, which is concerned with whether the internal ...

''S''=''T'' ⇔ ∀''s'' (''S''(''s'') ⇔ ''T''(''s'')). Since we have comprehension, induction can be a single statement rather than a schema. The analogous axiomatization of S1S is complete. However, for S2S, completeness is open (as of 2021). While S1S has uniformization, there is no S2S definable (even allowing parameters)

choice function A choice function (selector, selection) is a mathematical function ''f'' that is defined on some collection ''X'' of nonempty sets and assigns some element of each set ''S'' in that collection to ''S'' by ''f''(''S''); ''f''(''S'') maps ''S'' to ...

that given a non-empty set ''S'' returns an element of ''S'', and comprehension schemas are commonly augmented with various forms of the

axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...

. However, (1)-(4) is complete when extended with a determinacy schema for certain

parity game A parity game is played on a colored directed graph, where each node has been colored by a priority – one of (usually) finitely many natural numbers. Two players, 0 and 1, move a (single, shared) token along the edges of the graph. The owne ...

s. S2S can also be axiomatized by Π¹₃ sentences (using the prefix relation on strings as a primitive). However, it is not finitely axiomatizable, nor can it be axiomatized by Σ¹₃ sentences even if we add induction schema and a finite set of other sentences (this follows from its connection to Π¹₂-CA₀).

Theories related to S2S

For every finite ''k'', the monadic second order (MSO) theory of countable graphs with

treewidth In graph theory, the treewidth of an undirected graph is an integer number which specifies, informally, how far the graph is from being a tree. The smallest treewidth is 1; the graphs with treewidth 1 are exactly the trees and the forests. The gra ...

≤''k'' (and a corresponding tree decomposition) is interpretable in S2S (see

Courcelle's theorem In the study of graph algorithms, Courcelle's theorem is the statement that every graph property definable in the monadic second-order logic of graphs can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bru ...

). For example, the MSO theory of trees (as graphs) or of series-parallel graphs is decidable. Here (i.e. for bounded tree width), we can also interpret the finiteness quantifier for a set of vertices (or edges), and also count vertices (or edges) in a set modulo a fixed integer. Allowing uncountable graphs does not change the theory. Also, for comparison, S1S can interpret connected graphs of bounded

pathwidth In graph theory, a path decomposition of a graph is, informally, a representation of as a "thickened" path graph, and the pathwidth of is a number that measures how much the path was thickened to form . More formally, a path-decomposition ...

. By contrast, for every set of graphs of unbounded treewidth, its existential (i.e. Σ¹₁) MSO theory is undecidable if we allow predicates on both vertices and edges. Thus, in a sense, decidability of S2S is the best possible. Graphs with unbounded treewidth have large grid minors, which can be used to simulate a

Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...

. By reduction to S2S, the MSO theory of countable orders is decidable, as is the MSO theory of countable trees with their

Kleene–Brouwer order In descriptive set theory, the Kleene–Brouwer order or Lusin–Sierpiński order is a linear order on finite sequences over some linearly ordered set (X, <), that differs from the more commonly used

weakly compact cardinal In mathematics, a weakly compact cardinal is a certain kind of cardinal number introduced by ; weakly compact cardinals are large cardinals, meaning that their existence cannot be proven from the ZFC, standard axioms of set theory. (Tarski original ...

)). Also, an ordinal is definable using monadic second order logic on ordinals iff it can be obtained obtained from definable regular cardinals by ordinal addition and multiplication. S2S is useful for decidability of certain modal logics, with

Kripke semantics Kripke semantics (also known as relational semantics or frame semantics, and often confused with possible world semantics) is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Jo ...

naturally leading to trees. S2S+U (or just S1S+U) is undecidable if U is the unbounding quantifier — U''X'' Φ(''X'') iff Φ(''X'') holds for some arbitrarily large finite ''X''. However, WS2S+U, even with quantification over infinite paths, is decidable, even with S2S subformulas that do not contain U.

Formula complexity

A set of binary strings is definable in S2S iff it is regular (i.e. forms a

regular language In theoretical computer science and formal language theory, a regular language (also called a rational language) is a formal language that can be defined by a regular expression, in the strict sense in theoretical computer science (as opposed to ...

). In S1S, a (unary) predicate on sets is (parameter-free) definable iff it is an

ω-regular language The ω-regular languages are a class of ω-languages that generalize the definition of regular languages to infinite words. Formal definition An ω-language ''L'' is ω-regular if it has the form * ''A''ω where ''A'' is a regular language n ...

. For S2S, for formulas that use their free variables only on strings not containing a 1, the expressiveness is the same as for S1S. For every S2S formula φ(''S''₁,...,''S''_''k''), (with ''k'' free variables) and finite tree of binary strings ''T'', φ(''S''₁∩T,...,''S''_''k''∩T) can be computed in time linear in , ''T'', (see

), but as noted above, the overhead can be iterated exponential in the formula size (more precisely, the time is

O(, T, k)+2_^2

). For S1S, every formula is equivalent to a Δ¹₁ formula, and to a boolean combination of Π⁰₂ arithmetic formulas. Moreover, every S1S formula is equivalent to acceptance by a corresponding

ω-automaton In automata theory, a branch of theoretical computer science, an ω-automaton (or stream automaton) is a variation of finite automata that runs on infinite, rather than finite, strings as input. Since ω-automata do not stop, they have a variety o ...

of the parameters of the formula. The automaton can be a deterministic parity automaton: A parity automaton has an integer priority for each state, and accepts iff the highest priority seen infinitely often is odd (alternatively, even). For S2S, using tree automata (below), every formula is equivalent to a Δ¹₂ formula. Moreover, every S2S formula is equivalent to a formula with just four quantifiers, ∃''S''∀''T''∃''s''∀''t'' ... (assuming that our formalization has both the prefix relation and the successor functions). For S1S, three quantifiers (∃''S''∀''s''∃''t'') suffice, and for WS2S and WS1S, two quantifiers (∃''S''∀''t'') suffice; the prefix relation is not needed here for WS2S and WS1S. However, with free second order variables, not every S2S formula can be expressed in second order arithmetic through just Π¹₁ transfinite recursion (see

reverse mathematics Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...

). RCA₀ + (schema) is equivalent to (schema) . Over a base theory, the schemas are equivalent to (schema over ''k'') ∀''S''⊆ω ∃α₁<...<α_''k'' ''L''_α₁(''S'') ≺_Σ₁ ... ≺_Σ₁ ''L''_{α_''k''}(S) where ''L'' is the

constructible universe In mathematics, in set theory, the constructible universe (or Gödel's constructible universe), denoted by , is a particular class of sets that can be described entirely in terms of simpler sets. is the union of the constructible hierarchy . It w ...

(see also

large countable ordinal In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of rele ...

). Due to limited induction, Π¹₂-CA₀ does not prove that all true (under the standard decision procedure) Π¹₃ S2S statements are actually true even though each such sentence is provable Π¹₂-CA₀. Moreover, given sets of binary strings ''S'' and ''T'', the following are equivalent:
(1) ''T'' is S2S definable from some set of binary strings polynomial time computable from ''S''.
(2) ''T'' can be computed from the set of winning positions for some game whose payoff is a finite boolean combination of Π⁰₂(''S'') sets.
(3) ''T'' can be defined from ''S'' in arithmetic μ-calculus (arithmetic formulas +

least fixed-point logic In mathematical logic, fixed-point logics are extensions of classical predicate logic that have been introduced to express recursion. Their development has been motivated by descriptive complexity theory and their relationship to database query lan ...

)
(4) ''T'' is in the least β-model (i.e. an ω-model whose set-theoretic counterpart is transitive) containing ''S'' and satisfying all Π¹₃ consequences of in Π¹₂-CA₀.

Models of S1S and S2S

In addition to the standard model (which is the unique MSO model for S1S and S2S), there are other models for S1S and S2S, which use some rather than all subsets of the domain (see Henkin semantics). For every ''S''⊆ω, sets recursive in ''S'' form an elementary submodel of the standard S1S model, and same for every non-empty collection of subsets of ω closed under Turing join and Turing reducibility. This follows from relative recursiveness of S1S definable sets plus uniformization:
- φ(''s'') (as a function of ''s'') can be computed from the parameters of φ and the values of φ(''s'') for a finite set of ''s'' (with its size bounded by the number of states in a deterministic automaton for φ).
- A witness for ∃''S'' φ(''S'') can be obtained by choosing ''k'' and a finite fragment of ''S'' of ''S'', and repeatedly extending ''S'' such that the highest priority during each extension is ''k'' and that the extension can be completed into ''S'' satisfying φ without hitting priorities above ''k'' (these are permitted only for the initial ''S''). Also, by using lexicographically least shortest choices, there is an S1S formula φ' such that φ'⇒φ and ∃''S'' φ(''S'') ⇔∃!''S'' φ'(''S'') (i.e. uniformization; φ may have free variables not shown; φ' depends only on the formula φ). The minimal model of S2S consists of all

s on binary strings. It is an elementary submodel of the standard model, so if an S2S parameter-free definable set of trees is non-empty, then it includes a regular tree. A regular language can also be treated as a regular -labeled complete infinite binary tree (identified with predicates on strings). A labeled tree is regular if it can be obtained by unrolling a vertex-labeled finite directed graph with an initial vertex; a (directed) cycle in the graph reachable from the initial vertex gives an infinite tree. With this interpretation and encoding of regular trees, every true S2S sentence may already be provable in

elementary function arithmetic In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic,C. Smoryński, "Nonstandard Models and Related Developments" (p. 217). From ''Harvey Frie ...

. It is non-regular trees that may require nonpredicative comprehension for determinacy (below). There are nonregular (i.e. containing nonregular languages) models of S1S (and presumably S2S) (both with and without standard first order part) with a computable satisfaction relation. However, the set of recursive sets of strings does not form a model of S2S due to failure of comprehension and determinacy.

Decidability of S2S

The proof of decidability is by showing that every formula is equivalent to acceptance by a nondeterministic tree automaton (see

tree automaton A tree automaton is a type of state machine. Tree automata deal with tree structures, rather than the strings of more conventional state machines. The following article deals with branching tree automata, which correspond to regular languages of ...

and

infinite-tree automaton In computer science and mathematical logic, an infinite-tree automaton is a state machine that deals with infinite tree structures. It can be seen as an extension of top-down finite-tree automata to infinite trees or as an extension of infinite ...

). An infinite tree automaton starts at the root and moves up the tree, and accepts iff every tree branch accepts. A nondeterministic tree automaton accepts iff player 1 has a winning strategy, where player 1 chooses an allowed (for the current state and input) pair of new states (''p''₀,''p''₁), while player 2 chooses the branch, with the transition to p₀ if 0 is chosen and p₁ otherwise. For a co-nondeterministic automaton, all choices are by player 2, while for deterministic, (p₀,p₁) is fixed by the state and input; and for a game automaton, the two players play a finite game to set the branch and the state. Acceptance on a branch is based on states seen infinitely often on the branch; parity automata are sufficiently general here. For converting the formulas to automata, the base case is easy, and nondeterminism gives closure under existential quantifiers, so we only need closure under complementation. Using positional determinacy of parity games (which is where we need impredicative comprehension), non-existence of player 1 winning strategy gives a player 2 winning strategy ''S'', with a co-nondeterministic tree automaton verifying its soundness. The automaton can then be made deterministic (which is where we get an exponential increase in the number of states), and thus existence of ''S'' corresponds to acceptance by a non-deterministic automaton. ''Determinacy:'' Provably in ZFC, Borel games are determined, and the determinacy proof for boolean combinations of Π⁰₂ formulas (with arbitrary real parameters) also gives a strategy here that depends only on the current state and the position in the tree. The proof is by induction on the number of priorities. Assume that there are ''k'' priorities, with the highest priority being ''k'', and that ''k'' has the right parity for player 2. For each position (tree position + state) assign the least ordinal α (if any) such that player 1 has a winning strategy with all entered (after one or more steps) priority ''k'' positions (if any) having labels <α. Player 1 can win if the initial position is labeled: Each time a priority ''k'' state is reached, the ordinal is decreased, and moreover in between the decreases, player 1 can use a strategy for ''k''-1 priorities. Player 2 can win if the position is unlabeled: By the determinacy for ''k''-1 priorities, player 2 has a strategy that wins or enters an unlabeled priority ''k'' state, in which case player 2 can again use that strategy. To make the strategy positional (by induction on ''k''), when playing the auxiliary game, if two chosen positional strategies lead to the same position, continue with the strategy with the lower α, or for the same α (or for player 2) lower initial position (so we can switch a strategy finitely many times). ''Automata determinization:'' For determinization of co-nondeterministic tree automata, it suffices to consider ω-automata, treating branch choice as input, determinizing the automaton, and using it for the deterministic tree automaton. Note that this does not work for ''nondeterministic'' tree automata as the determinization for going left (i.e. ''s''→''s''0) can depend on the contents of the right branch; by contrast to nondeterminism, deterministic tree automata cannot even accept precisely nonempty sets. To determinize a nondeterministic ω-automaton ''M'' (for co-nondeterministic, take the complement, noting that deterministic parity automata are closed under complements), we can use a ''Safra tree'' with each node storing a set of possible states of ''M'', and node creation and deletion based on reaching high priority states. For details, see or. ''Decidability of acceptance:'' Acceptance by a nondeterministic parity automaton of the empty tree corresponds to a

on a finite graph ''G''. Using the above positional (also called memoryless) determinacy, this can be simulated by a finite game that ends when we reach a loop, with the winning condition based on the highest priority state in the loop. A clever optimization gives a quasipolynomial time algorithm, which is polynomial time when the number of priorities is small enough (which occurs commonly in practice). ''Theory of trees:'' For decidability of MSO logic on trees (i.e. graphs that are trees), even with finiteness and modular counting quantifiers for first order objects, we can embed countable trees into the complete binary tree and use the decidability of S2S. For example, for a node ''s'', we can represent its children by ''s''1, ''s''01, ''s''001, and so on. For uncountable trees, we can use Shelah-Stup theorem (below). We can also add a predicate for a set first order objects having cardinality ω₁, and the predicate for cardinality ω₂, and so on for infinite regular cardinals. Graphs of bounded tree width are interpretable using trees, and without predicates over edges this also applies to graphs of bounded clique width.

Combining S2S with other decidable theories

''Tree extensions of monadic theories:'' By Shelah-Stup theorem, if a monadic relational model ''M'' is decidable, then so is its tree counterpart. For example, (modulo choice of formalization) S2S is the tree counterpart of . In the tree counterpart, the first order objects are finite sequences of elements of ''M'' ordered by extension, and an ''M''-relation ''P''_''i'' is mapped to ''P''_''i'''(''vd''₁,...,''vd''_k) ⇔ ''P''_''i''(''d''₁,...,''d''_k) with ''P''_''i''' false otherwise (''d''_''j''∈''M'', and ''v'' is a (possibly empty) sequence of elements of ''M''). The proof is similar to the S2S decidability proof. At each step, a (nondeterministic) automaton gets a tuple of ''M'' objects (possibly second order) as input, and an ''M'' formula determines which state transitions are permitted. Player 1 (as above) chooses a mapping child⇒state that is permitted by the formula (given the current state), and player 2 chooses the child (of the node) to continue. To witness rejection by a non-deterministic automaton, for each (node, state) pick a set of (child, state) pairs such that for every choice, at least one of the pairs is hit, and such that all the resulting paths lead to rejection. ''Combining a monadic theory with a first order theory:''

Feferman–Vaught theorem Feferman–Vaught theorem in model theory is a theorem by Solomon Feferman and Robert Lawson Vaught that shows how to reduce, in an algorithmic way, the first-order theory of a product of first-order structures to the first-order theory of elemen ...

extends/applies as follows. If ''M'' is an MSO model and ''N'' is a first order model, then ''M'' remains decidable relative to a (Theory(''M''), Theory(''N''))

oracle An oracle is a person or agency considered to provide wise and insightful counsel or prophetic predictions, most notably including precognition of the future, inspired by deities. As such, it is a form of divination. Description The word '' ...

even if ''M'' is augmented with all functions ''M''→''N'' where ''M'' is identified with its first objects, and for each ''s''∈''M'' we use a disjoint copy of ''N'', with the language modified accordingly. For example, if ''N'' is (

\mathbb

,0,+,⋅), we can state ∀(function ''f'') ∀''s'' ∃''r''∈''N''_''s'' ''f''(''s'') +_{''N''_''s''} ''r'' = 0_{''N''_''s''}. If ''M'' is S2S (or more generally, the tree counterpart of some monadic model), the automata can now use ''N''-formulas, and thereby convert ''f'':''M''→''N''^''k'' into a tuple of ''M'' sets. Disjointness is necessary as otherwise for every infinite ''N'' with equality, the extended S2S or just WS1S is undecidable. Also, for a (possibly incomplete) theory ''T'', the theory ''T''^''M'' of ''M''-products of ''T'' is decidable relative to a (Theory(''M''), ''T'') oracle, where a model of ''T''^''M'' uses an arbitrary disjoint model ''N''_''s'' of ''T'' for each ''s''∈''M'' (as above, ''M'' is an MSO model; Theory(''N''_''s'') may depend on ''s''). The proof is by induction on formula complexity. Let ''v''_''s'' be the list of free ''N''_''s'' variables, including ''f''(''s'') if function ''f'' is free. By induction, one shows that ''v''_''s'' is only used through a finite set of ''N''-formulas with , ''v''_''s'', free variables. Thus, we can quantify over all possible outcomes by using ''N'' (or ''T'') to answer what is possible, and given a list possibilities (or constraints), formulate a corresponding sentence in ''M''. ''Coding into extensions of S2S:'' Every decidable predicate on strings can be encoded (with linear time encoding and decoding) for decidability of S2S (even with the extensions above) together with the encoded predicate. Proof: Given a nondeterministic infinite tree automaton, we can partition the set of finite binary labeled trees (having labels over which the automaton can operate) into finitely many classes such that if a complete infinite binary tree can be composed of same-class trees, acceptance depends only on the class and the initial state (i.e. state the automaton enters the tree). (Note a rough similarity with the

pumping lemma In the theory of formal languages, the pumping lemma may refer to: *Pumping lemma for regular languages, the fact that all sufficiently long strings in such a language have a substring that can be repeated arbitrarily many times, usually used to pro ...

.) For example (for a parity automaton), assign trees to the same class if they have the same predicate that given initial_state and set ''Q'' of (state, highest_priority_reached) pairs returns whether player 1 (i.e. nondeterminism) can simultaneously force all branches to correspond to elements of ''Q''. Now, for each ''k'', pick a finite set of trees (suitable for coding) that belong to the same class for automata 1-''k'', with the choice of class consistent across ''k''. To encode a predicate, encode some bits using ''k''=1, then more bits using ''k''=2, and so on.

References

Additional reference:
{{Cite book , last=Weyer , first=Mark , date=2002 , title=Automata, Logics, and Infinite Games , chapter=Decidability of S1S and S2S , series=Lecture Notes in Computer Science , volume=2500 , pages=207–230 , chapter-url=https://link.springer.com/chapter/10.1007/3-540-36387-4_12 , doi=10.1007/3-540-36387-4_12 , publisher=Springer, isbn=978-3-540-00388-5 Mathematical logic Computability theory Articles containing proofs